$\forall$${\it ds}$, ${\it da}$, $T$:Top, ${\it ks}$:Top List, ${\it upd}$:$x$:Knd$\times$Id fp$\rightarrow$ Top, $a$:Top, $i$, $j$:Id.
\\[0ex]R{-}has{-}loc(ecl{-}machine2($i$;${\it ds}$;${\it da}$;"ecl";$T$;${\it ks}$;$a$;${\it upd}$);$j$)
\\[0ex]$\sim$
\\[0ex]($\neg_{2}$null(update{-}spec{-}vars(${\it upd}$)) $\wedge_{2}$ $i$ = $j$)